es:event_system{i:l}, e',e,a:es-E(es).
(es-locl(es; e; a)  es-le(es; a; e'))
 ([e, e'] = append([e, es-pred(es; a)]; [a, e'])  (es-E(es) List)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, t  T, prop{i:l}, x. t(x), P  Q, P  Q, T, True, wellfounded{i:l}(A; x,y.R(x;y)), x(s), guard(T), P  Q, A c B
Lemmas	es-locl-wellfnd, es-E wf, es-locl wf, es-le wf, es-interval wf, append wf, es-pred wf, es-locl-iff, es-interval-less, es-le-trans3, event system wf, es-le-iff, es-pred-locl, append assoc, squash wf, true wf, es-le-pred, not wf, assert wf, es-first wf, es-interval-eq